Aspects of Incompleteness: Chapter 1 読書録1
Memo
index
Memo
以下,私が重要だと思うが特に番号が振られていない定理や補題はFact AやLem Bなどを振っておく.
今後数と言った場合はそれは自然数のことを指すとする. 面倒なので$ \vec{\cdot}と書いたらそれは$ \vec{k} = k_0,\dots,k_{n-1}のことを表すとする.
算術の言語$ \mathscr{L}_\mathbf{A}とは以下であり,有限である. 論理演算子: $ \lnot,\land,\lor,\to,\leftrightarrow,\forall,\exists 変項記号: $ vとプライム$ '
補助記号,カッコなど: $ (,),\lbrack,\rbrack
$ \lbrack,\rbrackは元の本には無いが,量化子を書くとゴチャゴチャになるため補助的に入れている
算術的な演算子
$ 0,S,+,\times
以下の略記を定める.
変項$ v_n = v \underbrace{'\cdots'}_{\text{$n$ times}}
数項$ \overline{\mathrm{n}} = \underbrace{S \cdots S}_{\text{$n$ times}} \mathrm{0}
すなわち
$ \overline{0}は$ 0
$ \overline{1}は$ S0
$ \overline{2}は$ SS0
論理式や文といったものは適当に定める.
変項は$ x,y,z,u,v,wなどを用いる.
数項は$ k,m,n,p,q,rなどを用いる.
Rmk
この区別は本には一切無く,私が便宜上採用しているだけに過ぎない.
数は立体$ \rm k,m,n,p,q,rで表すことにする. 数$ \rm kの数項を$ \overline{\rm{k}}とする.
文脈上明らかなとき,斜体$ kは$ \overline{\rm k}のこと,すなわち数項を指すとする. 文は$ \varphi, \psi, \theta,\chi
論理式は$ \alpha(x),\beta(x,y), \gamma(x), \xi(x), \eta(\vec{x})などを用いる.
項や論理式が統語論的に全く同じ形であることは$ \equivを使う.(元の本では$ :=だが分かりづらい)
例えば$ \mathrm{SS0} \equiv \overline{2}である.略記は適宜外す.
Def: 理論について
文の集合を理論という.$ Tとかで表す.
これらも同様に理論である.
文(あるいは公理)$ \varphiを$ Tに加えた集合$ T + \varphi
文の集合$ \Gammaを$ Tに加えた集合$ T + \Gamma
Memo
さしあたってこの本では1階述語論理の完全な演繹体系を$ \frak Lとして固定する. $ \mathfrak{L}によって生成される文の列を証明という.すなわち,証明列の末尾の文を証明している.
$ Tを仮定して$ \varphiの証明が存在する時,$ \varphiは$ Tで証明可能であり$ T \vdash \varphiと書く.
$ T \vdash \xi(\vec{x})すなわち$ \vec{x}が自由変項であるため$ \xi(\vec{x})が文になっていない(閉じていない)とき,これは$ T \vdash \forall\vec{x} \lbrack \xi(\vec{x}) \rbrackの略記とせよ.
$ Tの定理集合$ \mathrm{Th}(T) := \{ \varphi \mid T \vdash \varphi \}とする.
$ T \vdash \Gamma \iff \forall \varphi \in \Gamma:T \vdash \varphiと約束する.
$ T, T'が理論とする.
$ T \vdash T'なら↓という.
$ Tは$ T'の拡大理論(extension)
$ T'は$ Tの部分理論(subtheory)
Memo
$ \mathcal{N} = \lang \mathbb{N}, \mathrm{s}, +,\times, 0 \rangは算術の標準モデルという. 文$ \varphiが真であるとは,$ \mathcal{N}上で真であることを指す.
理論$ Tが真であるとは,$ Tの全ての文が真であることを指す.
$ \mathbf{Q1}\colon \forall x\forall y \lbrack Sx = Sy \to x = y \rbrack
$ \mathbf{Q2}\colon \forall x \lbrack \lnot 0 = Sx \rbrack
$ \mathbf{Q3}\colon \forall x \lbrack \lnot 0 = x \to \exists y(x = Sy) \rbrack
$ \mathbf{Q4} \colon \forall x \lbrack x + 0 = x \rbrack
$ \mathbf{Q5} \colon \forall x\forall y \lbrack x + Sy = S(x+y)) \rbrack
$ \mathbf{Q6} \colon \forall x \lbrack x \times 0 = 0 \rbrack
$ \mathbf{Q7} \colon \forall x\forall y \lbrack x \times Sy = x \times y + x \rbrack
以下の略記を定める.
$ x \neq y \equiv \lnot(x = y)
$ x \leq y \equiv \exists z \lbrack x + z = y \rbrack
$ x < y \equiv x \leq y \land x \neq y
Peano算術$ \bf PAは$ \bf Qに以下の帰納法を足したものである. 任意の論理式$ \alpha(x)に対して$ \mathbf{Ind}\colon\alpha(0) \land \forall x \lbrack \alpha(x) \to \alpha(\mathrm{s}x) \rbrack \to \forall x\lbrack\alpha(x)\rbrack
自明に$ \bf PA \vdash Q.
Fact 1
数$ \rm k,m,nとする.
1. $ \rm k \neq mであるとき,$ \mathbf{Q} \vdash \overline{\mathrm{k}} \neq \overline{\mathrm{m}}
2. $ \mathbf{Q} \vdash \overline{\rm k + m} = \overline{\rm k} + \overline{\rm m}
3. $ \mathbf{Q} \vdash \overline{\rm k \times m} = \overline{\rm k} \times \overline{\rm m}
すなわち,2と3が意味するのは,$ 1 + 4という式は$ \bf Q上において次のどちらで解釈しても良い.
数項$ \overline{5}
式$ \overline{1} + \overline{4}
$ \timesも同様
4. $ \mathbf{Q} \vdash x \leq \overline{\mathrm{n}} \to x = 0 \lor x = 1 \lor \cdots \lor x = \overline{\mathrm{m}}
5. $ \mathbf{Q} \vdash x \leq \overline{\mathrm{n}} \lor \overline{\mathrm{n}} \leq x
これらの事実より,あまりにも面倒なため数項を表す上線$ \overline{2}は随時省略する.
そもそも厳密に書くと忘れすぎる.
ただし$ \vec{\rm x}は数の自由変項であることに注意.
このとき,任意の数$ \vec{\rm{k}}に対し,以下を満たす論理式$ \delta_\mathrm{f}(\vec{x},y)が存在する.
1. $ \mathbf{Q} \vdash \delta_\mathrm{f}(\vec{\overline{\rm k}},\overline{\mathrm{y}}) \leftrightarrow \overline{\rm{y}} = \overline{\rm f(\vec{k})}
1'. $ \mathbf{Q} \vdash \delta_\mathrm{f}(\vec{k}, y) \leftrightarrow y = \overline{\rm f(\vec{k})}
2. $ \mathbf{PA} \vdash \delta_\mathrm{f}(\vec{x},y) \land \delta_\mathrm{f}(\vec{x},z) \to y = z
3. $ \mathbf{PA} \vdash \exists y\lbrack\delta_\mathrm{f}(\vec{x},y)\rbrack
remark
この事実は↓の方で可証再帰性という形で一般化される. 数上に定義される関数$ \rm f(\vec{x})に対し,以下を満たす論理式$ \delta_\mathrm{f}(\vec{x},y)が存在すれば,$ \rm fは$ T上で定義(define)される,という.
任意の数たち$ \rm \vec{k}に対し,$ T \vdash \delta_\mathrm{f}(\vec{k},y) \leftrightarrow y = \overline{\rm f(\vec{k})}
memo
他の文献では表現するとかとも言ったハズ.
memo
Fact2.1'は,任意の原始再帰的関数は$ \bf Q上で定義可能ということを述べている. a. 任意の(全域的な)再帰的関数も,$ \bf Q上で定義可能. 数上の関係$ \rm R(\vec{x})が$ T上で$ \rho(\vec{x})によって弱表現される(numerates)とは以下が成り立つこととする.
任意の$ \rm \vec{k}で,$ \mathrm{R}(\vec{\rm k}) \iff T \vdash \rho(\vec{k})
特に1項関係は集合と同一視できることを考えれば,
集合$ \rm Xが$ T上で$ \xi(x)によって弱表現されるとは
$ \mathrm{k} \in \mathrm{X} \iff T \vdash \xi(k)
が成り立つことである.
更に$ \rm R(\vec{x})が$ T上で$ \rho(\vec{x})によって表現される(binumerates)とは以下が成り立つこととする.
任意の$ \rm \vec{k}で,
$ \mathrm{R}(\vec{\rm k}) \iff T \vdash \rho(\vec{k})
$ \mathrm{R}^c(\vec{\rm k}) \iff T \vdash \lnot \rho(\vec{k})
ただし$ \mathrm{R}^cは$ \mathrm{R}の補集合を指す.
同様に,集合$ \rm Xが$ \xi上で表現されるとき,
$ \mathrm{k} \in \mathrm{X} \iff T \vdash \xi(k)かつ$ \mathrm{k} \notin \mathrm{X} \iff T \vdash \lnot\xi(k)
$ T上で$ \rhoによって表現される関係は,無矛盾な$ Tの拡大理論でも同じ$ \rhoで表現される.
memo
numerates及びbinumeratesの訳が思いつかなかったのでとりあえず菊池誠; "不完全性定理"に沿って弱表現/表現と訳した. Fact A
$ T上で弱表現される任意の関係は再帰的可算である a. $ \rm Rが再帰的関係$ \iff$ \rm Rが$ \bf Q上で表現可能 b. $ \rm Rが再帰的可算関係$ \iff$ \rm Rが$ \bf Q上で弱表現可能 proof of a.
$ \implies特性関数$ \chi_\mathrm{R}が再帰的 $ \implies$ \chi_\mathrm{R}は$ \bf Q上で定義可能(Fact3より)
$ \implies任意の数$ \rm \vec{k}に対し$ \mathbf{Q} \vdash \forall \vec{k}\forall y \left\lbrack \delta_{\chi_\mathrm{R}}(\vec{k},y) \leftrightarrow y = \overline{\rm \chi_\mathrm{R}(\vec{k})} \right\rbrackとなる$ \delta_{\chi_\mathrm{R}}が存在する.
特に特性関数の定義上$ y = \overline{0}または$ y = \overline{1}だから
$ \rho(\vec{k}) \equiv \delta_{\chi_\mathrm{R}}(\vec{k},\overline{0})とすれば
任意の$ \rm \vec{k}で
$ \mathrm{R}(\vec{\mathrm{k}}) \iff \chi_\mathrm{R} = 0 \iff \mathbf{Q} \vdash \rho(\vec{k})
$ \mathrm{R}^c(\vec{\mathrm{k}}) \iff \chi_\mathrm{R} = 1 \iff \mathbf{Q} \vdash \lnot\rho(\vec{k})
が成り立つので$ \rm Rは$ \bf Q上で表現される.
$ \impliedbyは$ \rhoから$ \delta_{\chi_\mathrm{R}}が作れるので良い.
proof of b.
$ \rm Rが再帰的可算関係$ \iff$ \rm R = \{ \vec{k} \mid \rm \chi(\vec{k}) = 0 \}となる再帰的な特性関数$ \chi_\mathrm{R}が存在する. より1.の証明と大体同じ.
Remark
Cor1より何らかの再帰的可算理論$ Tによって表現/弱表現されている任意の関係$ \rm Rは,$ \bf Q上でも表現可能/弱表現可能である. proof
$ \rm Rが$ Tで表現可能
$ \implies$ \rm Rは再帰的(Fact Aより)
$ \iff$ \rm Rは$ \bf Q上で表現可能(Cor 1より)
以下の略記を定める.$ xについての量化が有界であるという.
$ \exists x \leq y \lbrack \beta(x) \rbrack \equiv \exists x\lbrack x \leq y \land \beta(x) \rbrack
$ \forall x \leq y \lbrack \beta(x) \rbrack \equiv \forall x\lbrack x \leq y \to \beta(x) \rbrack
$ x < yも同様にする.
Def
$ \rm fが原始再帰的関数であり,Fact 2の条件を満たすような$ \delta_\mathrm{f}(\vec{x},y)について,
論理式$ \delta_\mathrm{f}(\vec{x},0)を厳密に原始再帰的 (primitive recursive in the strict sense / SPR)であると言う.
$ \mathrm{PR}はSPR論理式を含み,以下で閉じた論理式の集合とする.
論理演算
有界量化
自由変項を数項によって代入する操作
$ \xi \in Fかつ,原始再帰的な$ \rm fとFact2を満たす$ \delta_\mathrm{f}(\vec{x},y)について
$ \exists z \lbrack \delta_\mathbf{f}(\vec{x},z) \land \xi \rbrack
$ \forall z \lbrack \delta_\mathbf{f}(\vec{x},z) \to \xi \rbrack
$ \mathrm{PR}の要素である論理式を原始再帰的な論理式(primitive recursive / PR)という.
memo
おそらくなのだが,この後の展開的にPR論理式とは$ \Delta_0論理式のことだと考えても多分問題無いと思われる.
Memo
任意のPR論理式は$ \bf PA上では何らかのSPR論理式と同値である.
どのような論理式がPRであるか判断するにはFact2の証明の詳細に依る.
一方,詳細に依らずとも以下のCor 2が得られる.
論理式$ \eta(\vec{x})が$ T上で決定可能であるとは以下のこととする. 任意の$ \vec{k}について$ T \vdash \eta(\vec{k})または$ T \vdash \lnot\eta(\vec{k})
特に文$ \varphiが$ T上で決定可能であるとは以下のことを指す.
$ T \vdash \varphiまたは$ T \vdash \lnot \varphi
$ \rho(\vec{x})がPRであれば,$ \mathbf{Q} \vdash \rho(\vec{k})$ \iff$ \rho(\vec{k})が真
ここから更に,
1. 任意のPR論理式は$ \bf Q上で決定可能.
2. 関係$ \mathrm Rが原始再帰的$ \iff$ \bf Q上で$ \rm Rを表現するPR論理式が存在する.
remark
特に断り無く今後Cor2は用いられる.
Def
$ \rm Rを$ \bf Q上で表現するPR論理式を,$ \rm RのPR表現と呼ぶことにする.
$ \rm RのPR弱表現も同様に定める.
$ T \vdash \rm \bf PAとする.
$ \rm fが原始再帰的関数のとき,Fact 2より対応する論理式$ \delta_\mathrm{f}が存在する. そこで,関数記号$ \rm fを$ Tの言語に加え,次の公理を$ Tに加える
$ f(\vec{x}) = y \leftrightarrow \delta_\mathrm{f}(\vec{x},y)
この新しい理論を$ Sとすると,$ Sは$ Tの保存的拡大である. すなわち$ T \vdash \varphi \implies S \vdash \varphiである(ただし$ \varphiは$ Tの言語における論理式)
したがって,$ Tの言語に予め関数記号$ \rm fが入っていたと仮定しても,本質的に違いはないことが保証される.
よって今後は関数に対応して$ \mathscr{L}_\mathrm{A}を適当に拡張してよいことにし,この事実は断り無く用いられる.
Remark
Def: 補助的な原始再帰的関数
以下の補助的な原始再帰的関数を定義する.
ペア関数$ \lang k,m \rang = 2^k \times 3^m $ \rm (k)_mは次を返す関数とする.
$ \mathrm{k}を$ \mathrm{m}番目の素数の$ \mathrm{n}乗$ p_\mathrm{m}^\mathrm{n}で割っていくとして,割り切れる最大の$ \rm nとする.
ただし$ (0)_m = 0とする.
Remark
$ \rm (k)_mは数の有限列をエンコーディングする用途で使う.より端的には
数の有限列$ \rm n_0, \cdots,n_kに対し,$ (\mathrm{n})_\mathrm{i} = \mathrm{n}_\mathrm{i}(ただし$ \mathrm{i} < \mathrm{k})となるような$ \rm nが存在することを示す.
Observation
$ (\cdot)_\cdotは以下のような帰納的定義をバラすのに便利である.やってみましょう
$ \rm f(x)を以下のように定義する.
$ \rm f(0) = 0
$ \rm f(n + 1) = \left\{\begin{array}{ll} \mathrm{g(f(n), n)} & (\mathrm{n \in X})\\ \mathrm{h(f(n))} & (\mathrm{n \notin X})\end{array}\right.
ここで$ \rm g(x,y), h(x), Xは$ g,h,\xiなど表現されるものとする.
$ \delta(x,y)を以下のように定義する.
$ \delta(x,y) \equiv \exists z \lbrack (z)_{0} = 0 \land (z)_x = y \land \\ \forall u < x \lbrack \xi((z)_u) \to (z)_{u + 1} = g((z)_u,u) \rbrack \land \forall u < x \lbrack \lnot\xi((z)_u) \to (z)_{u+1} = h((z)_u) \rbrack \rbrack
$ \delta(x,y)は$ \mathrm{f}を$ \bf PA上で定義する.
更に$ \mathbf{PA}\vdash \forall x \exists y \forall z\lbrack \delta(x,z) \leftrightarrow z = y \rbrack
故に$ \mathscr{L}_\mathrm{A}に以下の関数記号$ fを追加及び,公理$ f(x) = y \leftrightarrow \delta(x,y)を入れて拡張しても本質的には変わらない.
そして以下が成り立つ.
$ \mathbf{PA} \vdash f(0) = 0
$ \mathbf{PA} \vdash \xi(x) \to f(x + 1) = g(f(x),x)
$ \mathbf{PA} \vdash \lnot\xi(x) \to f(x + 1) = h(f(x))
$ \mathscr{L}_\mathrm{A}のアルファベットを適当に並べた記号列のことを式と呼ぶことにする.
式は有効な項や論理式であるとは限らない.
逆に項や論理式は式である.
以下,Gödel数$ \rm xを持つ式を$ E_\mathrm{x}と表す.
a. 連結関数$ \cdot \frown \cdotは原始再帰的である.
連結関数とはGödel数$ \rm x,yを持つ式$ E_\mathrm{x},E_\mathrm{y}を繋げた式$ E_\mathrm{x}E_\mathrm{y}のGödel数を求める関数のことである.
remark
例えば1.より$ \mathrm{not}(\mathrm{x}) := \ulcorner \lnot \urcorner \frown \mathrm{x}も原始再帰的関数であるが,これは与えられた式$ E_\mathrm{x}に否定記号を付けた式$ \lnot E_\mathrm{x}のGödel数$ \ulcorner E_\mathrm{x} \urcornerを算出する関数である.
同様に$ \mathrm{imp}(\mathrm{x},\mathrm{y}) := \mathrm{x} \frown \ulcorner \to \urcorner \frown \mathrm{y}とかのように定義できる.
なおこれらはあくまで擬似的な定義の仕方である.2アリティの論理演算子をわざわざ中置にする本質的な意味はなく,実際の実装では$ \mathbin{\to}(E_\mathrm{x},E_\mathrm{y})のように考える
カッコも本質的な部分ではない.
b. 自由変項への数項の代入操作は原始再帰的である.
これを真面目に議論するには
c. 論理式の集合$ \mathrm{Form}及び文の集合$ \mathrm{Sent}は原始再帰的である.
おそらく言わんとしたいことは正確には
c'. 論理式のGödel数の集合や文のGödel数の集合は原始再帰的である
だと思うが,そのように明示的に書いてない
ref
テキストではすごくあっさり証明されているが,そんなに明らかではない.
以下を参照せよ
Remark
Thm 1より基本的に原始再帰的理論について調べればよいので,今後は断りがなければ理論は原始再帰的とする. また断りがなければ理論は無矛盾で,$ \bf Qの拡大とする.